p:FinProbSpace, A, B:p-open(p). p-union(A;B)  p-open(p) 

latex

Definitions	FinProbSpace, t  T, #$n, x:A. B(x), {i..j}, Outcome, {x:A| B(x)} , , x:AB(x), Type, A  B, S  T, P & Q, i  j < k, suptype(S; T), <a, b>, f(a), x:A  B(x), x.A(x), a < b, Void, P  Q, False, A, p-union(A;B), p-open(p), if b then t else f fi , , (i = j), s = t, , b, b, , P  Q, Unit, left + right
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bool wf, bnot wf, not wf, assert wf, ifthenelse wf, eq int wf, le wf, nat wf, p-outcome wf, int seg wf, finite-prob-space wf